Skip to content

[experiment] Special handling of root node in AcyclicGraph algorithm#22014

Draft
ppedrot wants to merge 3 commits intorocq-prover:masterfrom
ppedrot:acyclic-graph-explicit-root
Draft

[experiment] Special handling of root node in AcyclicGraph algorithm#22014
ppedrot wants to merge 3 commits intorocq-prover:masterfrom
ppedrot:acyclic-graph-explicit-root

Conversation

@ppedrot
Copy link
Copy Markdown
Member

@ppedrot ppedrot commented May 10, 2026

The most expensive kind of level constraint in the current algorithm is of the form "enforce u ≤ Set". Indeed the forward pass has to crawl basically the whole graph starting from Set, as all levels are above Set. This is the worst case for the complexity of our variant of of the Tarjan algorithm, which expects the graph to be sparse. Unfortunately, in practice such constraints seem to be commonplace in universe-polymorphic code.

To work around this issue, in this PR we try to handle Set in a special way by not storing it in the graph as a normal node. Instead we assume "Set ≤ u" implicitly everywhere, and we only keep a set of constraints "Set < u". We still have to perform a kind of forward pass to merge a level with Set, but we do so hopefully efficiently by leveraging the topological order maintained by the algorithm. We add in particular a map to quickly access nodes by their topological index.

@ppedrot ppedrot added request: full CI Use this label when you want your next push to trigger a full CI. kind: experiment labels May 10, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 10, 2026
@ppedrot
Copy link
Copy Markdown
Member Author

ppedrot commented May 10, 2026

@coqbot bench

@ppedrot
Copy link
Copy Markdown
Member Author

ppedrot commented May 10, 2026 •
edited
Loading

@SkySkimmer the bench died with a weird error in an unrelated script... Any idea what went wrong?

@ppedrot
Copy link
Copy Markdown
Member Author

ppedrot commented May 10, 2026

Let's retry: @coqbot bench

@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented May 10, 2026

That error happens when we tell it to bench an empty package. I did a manual run and opened #22015

@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented May 11, 2026

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│          rocq-metarocq-translations │   14.99    15.86  -5.49 │   108558881590    111365221376  -2.52 │  777552   779644  -0.27 │
│                 rocq-metarocq-pcuic │  611.46   646.88  -5.48 │  3951399127602   4126818571618  -4.25 │ 2452448  2449736   0.11 │
│           rocq-metarocq-safechecker │  325.79   342.60  -4.91 │  2436993196139   2517526121624  -3.20 │ 1833880  1851892  -0.97 │
│                         rocq-stdlib │  425.03   435.09  -2.31 │  1518889931048   1555547024749  -2.36 │  634144   629892   0.68 │
│              rocq-metarocq-template │   81.85    83.35  -1.80 │   561854974328    570313500092  -1.48 │ 1088628  1088780  -0.01 │
│                            coq-corn │  647.09   658.23  -1.69 │  4403201841913   4454286943687  -1.15 │  750268   767868  -2.29 │
│                 coq-category-theory │  543.38   552.66  -1.68 │  3984963058285   4057393588920  -1.79 │  882356   926624  -4.78 │
│         coq-rewriter-perf-SuperFast │  467.01   474.31  -1.54 │  3662825064454   3715715340399  -1.42 │ 1263188  1251060   0.97 │
│ coq-neural-net-interp-computed-lite │  235.51   238.10  -1.09 │  2265331102422   2266678207010  -0.06 │  880188   882628  -0.28 │
│                            coq-hott │  157.54   158.98  -0.91 │  1061606859476   1074624009712  -1.21 │  479996   468664   2.42 │
│                         coq-coqutil │   47.11    47.50  -0.82 │   292370927623    293490859894  -0.38 │  563812   563296   0.09 │
│          rocq-mathcomp-finite-group │   26.58    26.76  -0.67 │   173283319582    173307680277  -0.01 │  574428   574324   0.02 │
│              rocq-mathcomp-solvable │   98.97    99.56  -0.59 │   672726629099    672948198825  -0.03 │ 1115000  1123172  -0.73 │
│               rocq-metarocq-erasure │  474.37   476.85  -0.52 │  3267291344818   3266179685910   0.03 │ 1818196  1792252   1.45 │
│                  rocq-mathcomp-boot │   39.49    39.62  -0.33 │   233085532024    233266453589  -0.08 │  654256   659484  -0.79 │
│                 rocq-mathcomp-field │  193.38   193.87  -0.25 │  1454868350017   1453100357219   0.12 │ 2281992  2290612  -0.38 │
│                           coq-color │  231.04   231.39  -0.15 │  1468255985042   1469397354135  -0.08 │ 1147048  1167740  -1.77 │
│  rocq-mathcomp-group-representation │  104.08   104.20  -0.12 │   732461553034    730955120362   0.21 │ 1705632  1707512  -0.11 │
│                         coq-unimath │ 1831.36  1833.17  -0.10 │ 15274634817397  15273718525007   0.01 │ 1097004  1094016   0.27 │
│          coq-performance-tests-lite │  898.73   899.24  -0.06 │  7196791476902   7226541964741  -0.41 │ 1292992  1232548   4.90 │
│              coq-mathcomp-odd-order │  605.64   605.86  -0.04 │  4315240897623   4308776413135   0.15 │ 2607360  2639600  -1.22 │
│        coq-fiat-crypto-with-bedrock │ 7289.07  7285.49   0.05 │ 60131988663178  60077141160500   0.09 │ 2955444  2973732  -0.61 │
│                        rocq-runtime │   76.26    76.22   0.05 │   551046467920    550778290697   0.05 │  494660   494812  -0.03 │
│                        coq-rewriter │  332.36   332.12   0.07 │  2474704293805   2472571299773   0.09 │ 1444448  1464564  -1.37 │
│                      coq-verdi-raft │  494.97   493.97   0.20 │  3426517970386   3429738973318  -0.09 │  814556   817640  -0.38 │
│                           coq-verdi │   43.46    43.37   0.21 │   289643619192    290202147474  -0.19 │  528800   526168   0.50 │
│                        coq-coqprime │   53.29    53.11   0.34 │   361514118594    362981842129  -0.40 │  826208   824204   0.24 │
│                            coq-core │    2.79     2.78   0.36 │    18563444620     18575554727  -0.07 │   90952    90848   0.11 │
│               rocq-mathcomp-algebra │  331.24   330.03   0.37 │  2436472408872   2434607458108   0.08 │ 1356308  1353428   0.21 │
│               coq-engine-bench-lite │  129.29   128.71   0.45 │   961829159809    959860837113   0.21 │ 1004388  1106036  -9.19 │
│                    coq-math-classes │   83.24    82.81   0.52 │   503911201120    503152900939   0.15 │  515612   513928   0.33 │
│                 rocq-mathcomp-order │   81.60    81.17   0.53 │   600909199023    600196048239   0.12 │ 1606868  1591680   0.95 │
│                        rocq-bignums │   25.40    25.24   0.63 │   159905544080    160206636438  -0.19 │  458952   458528   0.09 │
│                           rocq-elpi │   16.39    16.27   0.74 │   116100224255    116230717490  -0.11 │  448672   448548   0.03 │
│                        coq-bedrock2 │  361.31   358.34   0.83 │  2998304440900   2992679401375   0.19 │  834232   830760   0.42 │
│                      coq-coquelicot │   39.60    39.22   0.97 │   238168685023    237191779121   0.41 │  830128   827216   0.35 │
│                rocq-metarocq-common │   41.47    41.04   1.05 │   269345022389    263485205960   2.22 │  896508   898576  -0.23 │
│                       coq-fourcolor │ 1368.33  1353.68   1.08 │ 12484246808307  12449128108198   0.28 │ 1272468  1016084  25.23 │
│               coq-mathcomp-analysis │ 1168.67  1155.46   1.14 │  8519455963757   8414702394384   1.24 │ 1965788  1961688   0.21 │
│                       coq-fiat-core │   55.84    55.07   1.40 │   337247894774    338353712454  -0.33 │  484620   482068   0.53 │
│                    coq-fiat-parsers │  281.52   277.17   1.57 │  2146994999577   2124883428157   1.04 │ 2270300  2272224  -0.08 │
│                 rocq-metarocq-utils │   24.65    24.26   1.61 │   160812530471    157553950334   2.07 │  608808   591260   2.97 │
│                           rocq-core │    6.83     6.72   1.64 │    41397321147     41665297977  -0.64 │  445412   445048   0.08 │
│                      rocq-equations │    8.59     8.45   1.66 │    58934372330     59209646860  -0.46 │  405008   400644   1.09 │
│                   coq-iris-examples │  371.86   364.86   1.92 │  2431376514865   2394909605759   1.52 │ 1111108  1086176   2.30 │
│             rocq-mathcomp-ssreflect │    1.12     1.09   2.75 │     7165344566      7114420191   0.72 │  591632   591508   0.02 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-compcert (dependency install failed in NEW)

coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SLOW DOWNS                                                             │
│                                                                                                                                          │
│  OLD     NEW    DIFF     %DIFF     Ln                     FILE                                                                           │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   11.9   18.2  6.3512     53.51%   118  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                     │
│   62.8   64.5  1.6061      2.56%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                      │
│   5.22   6.65  1.4352     27.52%  1346  coq-fiat-crypto-with-bedrock/src/Assembly/Symbolic.v.html                                        │
│   44.1   45.5  1.3076      2.96%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                 │
│   42.6   43.9  1.2823      3.01%   578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                 │
│   5.38   6.63  1.2436     23.10%   247  coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapBool.v.html                                      │
│   7.03   8.10  1.0683     15.20%   552  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│ 0.0103   1.08  1.0657  10316.61%    25  rocq-metarocq-erasure/erasure/theories/EEtaExpandedFix.v.html                                    │
│   38.6   39.6  1.0560      2.74%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│   1.95   2.81  0.8586     44.06%  1003  coq-fiat-crypto-with-bedrock/src/Assembly/Symbolic.v.html                                        │
│   94.0   94.9  0.8446      0.90%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│   1.60   2.41  0.8082     50.47%   309  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v.html          │
│   4.67   5.48  0.8036     17.20%    66  coq-category-theory/Instance/Lambda/Eval.v.html                                                  │
│   3.32   4.08  0.7575     22.83%   996  coq-fiat-crypto-with-bedrock/src/Assembly/Symbolic.v.html                                        │
│    237    237  0.6969      0.29%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                       │
│  0.377   1.03  0.6498    172.15%   565  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/redc.v.html                    │
│   2.86   3.49  0.6280     21.98%  3602  rocq-metarocq-erasure/erasure/theories/Typed/OptimizeCorrectness.v.html                          │
│   27.4   28.0  0.6273      2.29%   148  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                     │
│   29.2   29.8  0.6105      2.09%   145  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                     │
│   13.4   14.0  0.6029      4.49%   216  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                         │
│   1.72   2.31  0.5854     34.04%    38  coq-category-theory/Instance/Lambda/Exp.v.html                                                   │
│   2.17   2.72  0.5517     25.43%   516  rocq-metarocq-common/common/theories/UniversesDec.v.html                                         │
│  0.274  0.819  0.5449    198.85%   389  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/RecodeProofs.v.html                                │
│   1.86   2.40  0.5367     28.83%   967  rocq-metarocq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html                          │
│   1.56   2.09  0.5292     33.98%    42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                         │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SPEED UPS                                                           │
│                                                                                                                                      │
│  OLD    NEW     DIFF     %DIFF    Ln                    FILE                                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  3.03   0.583  -2.4428  -80.74%  1479  rocq-metarocq-pcuic/pcuic/theories/PCUICSubstitution.v.html                                   │
│   202     200  -2.4232   -1.20%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│  2.75   0.376  -2.3753  -86.32%   102  coq-fiat-parsers/src/Parsers/ParserImplementation.v.html                                      │
│  1.81   0.268  -1.5448  -85.20%    78  rocq-metarocq-pcuic/pcuic/theories/PCUICConversion.v.html                                     │
│  1.66   0.317  -1.3455  -80.96%  2493  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                        │
│  1.57   0.230  -1.3429  -85.40%  2601  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                        │
│  36.2    34.8  -1.3176   -3.64%   195  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│  1.28   0.197  -1.0820  -84.59%   395  rocq-metarocq-pcuic/pcuic/theories/PCUICElimination.v.html                                    │
│  1.25   0.202  -1.0525  -83.87%   278  rocq-metarocq-pcuic/pcuic/theories/Bidirectional/BDUnique.v.html                              │
│  1.21   0.165  -1.0443  -86.34%   266  rocq-metarocq-pcuic/pcuic/theories/Bidirectional/BDUnique.v.html                              │
│  1.18   0.177  -1.0016  -85.02%   298  rocq-metarocq-pcuic/pcuic/theories/Bidirectional/BDUnique.v.html                              │
│  22.1    21.3  -0.8072   -3.65%   520  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│ 0.841  0.0378  -0.8031  -95.50%   245  rocq-metarocq-pcuic/pcuic/theories/PCUICSR.v.html                                             │
│  56.5    55.8  -0.7838   -1.39%   516  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│  1.07   0.290  -0.7833  -73.00%   770  rocq-metarocq-pcuic/pcuic/theories/PCUICEquality.v.html                                       │
│  3.89    3.13  -0.7623  -19.58%   250  rocq-metarocq-erasure/erasure/theories/EWellformed.v.html                                     │
│ 0.813  0.0567  -0.7564  -93.03%   383  rocq-metarocq-pcuic/pcuic/theories/PCUICClassification.v.html                                 │
│  55.8    55.1  -0.7468   -1.34%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                      │
│ 0.861   0.117  -0.7439  -86.41%  2583  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                        │
│ 0.836  0.0925  -0.7436  -88.94%  1801  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                        │
│ 0.870   0.129  -0.7405  -85.13%   407  rocq-metarocq-pcuic/pcuic/theories/PCUICConvCumInversion.v.html                               │
│ 0.863   0.127  -0.7360  -85.28%  1815  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                        │
│ 0.898   0.165  -0.7329  -81.64%  2470  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                        │
│ 0.847   0.124  -0.7240  -85.43%  2151  rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                        │
│ 0.758  0.0420  -0.7156  -94.45%    59  rocq-metarocq-pcuic/pcuic/theories/PCUICConvCumInversion.v.html                               │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label May 11, 2026
@ppedrot ppedrot force-pushed the acyclic-graph-explicit-root branch from e487b6c to 1561417 Compare May 11, 2026 08:31
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 11, 2026
ppedrot added 3 commits May 11, 2026 10:31
@ppedrot
Allow setting a root in AcyclicGraph.
f69fce1 
We do not have to explicitly register it when building the empty graph.
@ppedrot
Keep track of components in AcyclicGraph data structure.
39cbebe
@ppedrot
Remove root from AcyclicGraph internal graph.
bfc706e 
The most expensive kind of level constraint in the current algorithm is of the
form "enforce u ≤ Set". Indeed the forward pass has to crawl basically the whole
graph starting from Set, as all levels are above Set. This is the worst case for
the complexity of our variant of the Tarjan algorithm, which expects the graph to
be sparse. Unfortunately, in practice such constraints seem to be commonplace in
universe-polymorphic code.

To work around this issue, in this commit we try to handle Set in a special way
by not storing it in the graph as a normal node. Instead we assume "Set ≤ u"
implicitly everywhere, and we only keep a set of constraints "Set < u". We
still have to perform a kind of forward pass to merge a level with Set, but we
do so hopefully efficiently by leveraging the topological order maintained by
the algorithm.
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label May 11, 2026
@ppedrot ppedrot force-pushed the acyclic-graph-explicit-root branch from 1561417 to bfc706e Compare May 11, 2026 08:32
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 11, 2026
@ppedrot
Copy link
Copy Markdown
Member Author

ppedrot commented May 11, 2026

The new version has the same fast-paths in the graph traversal for Set as for the normal algorithm. On the slowest line from fiat-parser it seems to be much faster. Let's see if this actually works on a new bench. @coqbot bench

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

kind: experiment

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ppedrot @SkySkimmer